es:ES, i, x, y, z:Id, Tx, Ty, Tz:Type, P:(TxTyTz), Lx, Ly, Lz:(Knd List).
@i only Lx affect x:Tx
 @i only Ly affect y:Ty
 @i only Lz affect z:Tz
 @i(x:Tx)
 @i(y:Ty)
 @i(z:Tz)
 e@i.
 (kind(e)  Lx @ Ly @ Lz)
  P(x when e,y when e,z when e)
  P((x after e),(y after e),(z after e))
 @i stable state.P(state.x,state.y,state.z)   

latex

Definitions

ES, t  T, type List, x:A. B(x), E, left + right, P  Q, P  Q, x:AB(x), x(s1,s2,s3), , P  Q, x:A  B(x), P & Q, P  Q, False, A, Void, x when e, (x after e), <a, b>, s = t, f(a), Type, Dec(P), e@i. P(e), vartype(i;x), @i(x:T), {T}, SQType(T), Id, s ~ t, Atom$n, let x,y = A in B(x;y), t.1, loc(e), b, b, , discrete(i;x), Unit, if b then t else f fi , (discrete state after e), (discrete state when e), @i stable state.P(state)  , s.x, {x:A| B(x)} , A c B, @i only L affect x:T, x. t(x), Knd, as @ bs, kind(e), (x  l)

Lemmas

alle-at wf, es-dtype wf, es-frame wf, es-after wf, es-loc wf, eqtt to assert, eqff to assert, assert of bnot, es-isconst wf, bool wf, bnot wf, not wf, assert wf, es-when wf, Id wf, Id sq, es-vartype wf, decidable l member, decidable equal Kind, iff transitivity, or functionality wrt iff, member append, append wf, l member wf, es-kind wf, es-E wf, Knd wf, event system wf